CHOICE-STRATEGY-IS: 
@(SUPPORT C2);

EDIT-STRATEGY-IS: 
α(C)>3∨∂(C)>4;


PARMODULATE =T
EQUAL-SYMBOL ==
PAR-DEPTH-BOUND =3
ELAPSED-TIME =10867

NIL 1 2
1 (x * N)= x;A2B
2 ¬(rev(lemmaA1(EDI4))* lemmaA2(EDI4))= rev(EDI4);THEOREM